﻿using System;
using System.Collections.Generic;
using System.ComponentModel;
using System.Data;
using System.Drawing;
using System.Linq;
using System.Text;
using System.Windows.Forms;
using System.Text.RegularExpressions;

/*
 * Authors:
 * Matt Rudnick
 * Clay Smith
 * Mridul Bhattarai 
 * 
 * Purpose: To demonstrate two AI algorithms
 * WalkSAT and Resolution
 * 
 */
namespace AIproject
{
    public partial class AI_Project : Form
    {
        List<Clause> set_of_clauses; //set of clauses
        Model main_model;
        Regex regex; //= new Regex(
        public AI_Project()
        {
            InitializeComponent();
            main_model = new Model();
            set_of_clauses = new List<Clause>();
        }


        /// <summary>
        /// count number of satisfied clauses
        /// </summary>
        /// <returns>number of satified clauses</returns>
        public int count_satisfied_clauses()
        {
            int count = 0;
            foreach (Clause c in set_of_clauses)
            {
                if (c.evaluate())
                    count++;
            }
            return count;
        }

        /// <summary>
        /// generate a set of false clauses
        /// </summary>
        /// <returns>List of false clauses</returns>
        private List<Clause> gen_set_of_false_clauses()
        {
            List<Clause> false_list = new List<Clause>();
            foreach (Clause c in set_of_clauses)
            {
                if (c.evaluate() == false) //evaluates to false
                    false_list.Add(c); //add to the list
            }
            return false_list;
        }

        /// <summary>
        /// choose a completely random false clause
        /// </summary>
        /// <returns>return a single false clause</returns>
        private Clause pick_random_false_clause()
        {
            List<Clause> false_list = gen_set_of_false_clauses();
            Random rnd = new Random();
            int num = rnd.Next(0, false_list.Count - 1); //get random index
            return false_list[num]; //return that item
        }

        /// <summary>
        /// returns the evaluation of this clause
        /// </summary>
        /// <returns>true if evaluates to true and false if evaluates to false</returns>
        private bool evaluate_clauses() //List<Clause> set_of_clauses
        {
            foreach (Clause c in set_of_clauses)
            {
                if (!(c.evaluate())) //if any of these evaluate to false
                    return false; //the clause is false
            }//end foreach
            return true; //the clause is true;
        }

        /// <summary>
        /// build a clause
        /// </summary>
        /// <param name="clauseString">the string that needs to be interpreted as a clause</param>
        /// <returns>the constructed instance of the clause class</returns>
        private Clause buildClause(string clauseString)
        {
            string tempstr;
            Clause newClause = new Clause(main_model);
            
            if (clauseString == null || clauseString.Length == 0)
            {
                return newClause; //empty clause
            }
            newClause.original_clause = clauseString;
            clauseString = clauseString.Trim();
            while(clauseString.Contains('|'))
            {
                tempstr = clauseString.Substring(0, clauseString.IndexOf('|'));
                clauseString = clauseString.Substring(clauseString.IndexOf('|')+1);
                //cuts the string down
                newClause.Add(buildLiteral(tempstr));
            }
            if (clauseString.Length > 0)
            {
                newClause.Add(buildLiteral(clauseString));
            }
            return newClause; //return the newly constructed clause
        }

        /// <summary>
        /// create a literal from the string
        /// </summary>
        /// <param name="literalString">string which represents the literal</param>
        /// <returns>new constructed Literal</returns>
        private Literal buildLiteral(string literalString)
        {
            Literal literal1 = new Literal(main_model);
            if (literalString == null || literalString.Length==0)
            {
                return literal1;
            }
            literalString = literalString.Trim();
            // if it begins with a negation
            if(literalString[0].Equals('-'))
            {
                literal1.isNegation=true; //is a negation
                literal1.SymbolName = literalString.Substring(1);//, literalString.Length);
                //if the symbol has not previously been seen then add it
                if (!main_model.ContainsKey(literal1.SymbolName))
                    main_model.Add(literal1.SymbolName, true);
                return literal1;
            }
            literal1.isNegation = false;
            literal1.SymbolName = literalString;
            //if the symbol has not previously been seen then add it
            if (!main_model.ContainsKey(literal1.SymbolName))
                main_model.Add(literal1.SymbolName, true);
            return literal1; //return the created literal
        }//end buildLiteral

        /// <summary>
        /// Run button press event
        /// </summary>
        /// <param name="sender"></param>
        /// <param name="e"></param>
        private void runWalkSat_Click(object sender, EventArgs e)
        {
            //run the WalkSAT algoirthm given the form values
            if (runWalkSat(Convert.ToDouble(numericProb.Value), Convert.ToInt16(numericFlips.Value)))
            {
                //model is ok
                string tempStr;
                modelListBox.Items.Clear();
                foreach (KeyValuePair<string, bool> kvp in main_model)
                {
                    tempStr = kvp.Key;
                    tempStr = tempStr + "  =  ";
                    if (kvp.Value == true) //show true
                        tempStr += "TRUE";
                    else
                        tempStr += "FALSE";   //show false
                    modelListBox.Items.Add(tempStr); //add to output
                }
                MessageBox.Show("WalkSAT success");
            }
            else
            {
                modelListBox.Items.Clear();
                MessageBox.Show("WalkSAT failure"); //walkSat not successful
            }
            //this will start the running of the program
        }

        /// <summary>
        /// Make sure all items are in the model
        /// </summary>
        private void sync_main_model()
        {
            main_model.Clear(); //empty the model
            foreach (Clause c in set_of_clauses)
            {
                foreach (Literal l in c)
                {
                    if (!main_model.ContainsKey(l.SymbolName))
                        main_model.Add(l.SymbolName, true); //add the item value does not matter
                }
            }
        }

        /// <summary>
        /// Run the Walksat Algorithm
        /// </summary>
        /// <param name="p">probability</param>
        /// <param name="max_flips">maximum number of flips</param>
        /// <returns>true if found false if not found</returns>
        private bool runWalkSat(double p, int max_flips)
        {
            sync_main_model();
            Random random = new Random();
            Clause walkSat_clause;
            main_model.randomAssignment(); //randomly set the values
            for (int i = 0; i < max_flips; i++) //run until max flips
            {
                if (this.evaluate_clauses())
                    return true; //return true
                walkSat_clause = pick_random_false_clause();
                if (random.NextDouble() <= p) //if under probability
                {
                    //flip value
                    main_model.flip(walkSat_clause.grab_random_symbol_name());
                }
                else
                {
                    flip_best_symbol(walkSat_clause);
                }
            }//end for
            return false; //failure
        }

        /// <summary>
        /// find the best symbol to flip and flip it
        /// </summary>
        /// <param name="walkSat_clause">clause</param>
        private void flip_best_symbol(Clause walkSat_clause)
        {
            
            int bestCount = -1;
            int tempcount;
            string bestSymbol = "";
            foreach (Literal lit in walkSat_clause)
            {
                main_model.flip(lit.SymbolName);
                tempcount = this.count_satisfied_clauses();
                if (tempcount > bestCount)
                {
                    bestCount = tempcount; //best
                    bestSymbol = lit.SymbolName;
                }
                main_model.flip(lit.SymbolName); //flip it back;
            }
            if (bestSymbol != "")
            {
                main_model.flip(bestSymbol); //flip the best
            }
            else
            {
                throw new Exception("possible Error in flip_best_symbol");
            }
        }


        /// <summary>
        /// Checks to see if the string is legal
        /// </summary>
        /// <param name="strToCheck"></param>
        /// <returns></returns>
            public bool IsLegal(string strToCheck)
            {
                Regex objAlphaNumericPattern=new Regex("[^a-zA-Z]");
                //Regex clause_form = new Regex("^(-)[a-zA-z]+(|)(-)[a-zA-Z]*");
                Regex alphabet = new Regex("[a-zA-Z]");
                //if not alphabetic
                if(objAlphaNumericPattern.IsMatch(strToCheck))
                {
                    string newStr = strToCheck.Replace("-"," ");
                    newStr = newStr.Replace('|',' ');
                    if(alphabet.IsMatch(newStr)) //is a letter or space
                        return true; //string is legal
                    return false; //string is not legal
                }
                else //it is alphabetic
                {
                    return true; //the string is legal
                }
            }

        private void listBox1_SelectedIndexChanged(object sender, EventArgs e)
        {

        }

        private void toolTip1_Popup(object sender, PopupEventArgs e)
        {
         
        }

        /// <summary>
        /// call when add clause button is pressed
        /// </summary>
        /// <param name="sender"></param>
        /// <param name="e"></param>
        private void addClausebutton_Click(object sender, EventArgs e)
        {
            string x = textBoxClause.Text; //clause to add
            if (x != null && IsLegal(x)) //if clause is legal
            {
                try
                {
                    set_of_clauses.Add(buildClause(x));
                    listBoxClauses.Items.Add(x);
                }
                catch (Exception ex)
                {
                    MessageBox.Show("Error Parsing String");
                }
            }
            else
            {
                MessageBox.Show("Illegal Clause");
            }
        }

        /// <summary>
        /// remove the selected clause button
        /// </summary>
        /// <param name="sender"></param>
        /// <param name="e"></param>
        private void removeClauseButton_Click(object sender, EventArgs e)
        {
            string item;
            try{
               
                item = listBoxClauses.SelectedItem.ToString();
            }
            catch
            {
                return;
            }
            try{
                //listBoxClauses.Items.Remove(listBoxClauses.SelectedItem);
            //(string)listBoxClauses.SelectedItem;
            Clause removeMe = new Clause(main_model);
            foreach (Clause c in set_of_clauses)
            {
                if (c.original_clause.Equals(item))
                {
                    removeMe = c;
                    break; //found jump out
                }
            }
            set_of_clauses.Remove(removeMe);
            listBoxClauses.Items.Remove(listBoxClauses.SelectedItem);
            }
        catch(Exception ex)
         {
            MessageBox.Show("An error may have occured while trying to remove a clause");
        }
        }

        private void listBox1_SelectedIndexChanged_1(object sender, EventArgs e)
        {

        }

        /// <summary>
        /// given a List of Clause items clone it and return the clone
        /// </summary>
        /// <param name="list">List of Clause items</param>
        /// <returns>clone of the list</returns>
        private List<Clause> clone_list_of_clauses(List<Clause> list)
        {
            List<Clause> newList = new List<Clause>();
            foreach (Clause c in list)
            {
                newList.Add(c.clone());
            }
            return newList;
        }

        /// <summary>
        /// gets the final result
        /// </summary>
        /// <param name="clauses"></param>
        /// <returns>true or false</returns>
        private bool resolution(List<Clause> clauses)
        {
            clauses = clone_list_of_clauses(clauses);
            List<Clause> resolvents = new List<Clause>();//new Clause(main_model);
            List<Clause> newItem = new List<Clause>();
            //set_of_clauses
            while (true)
            {
                for (int i = 0; i < clauses.Count; i++)
                {
                    for (int j = 0; j < clauses.Count; j++)
                    {
                        if (clauses[i] != clauses[j]) //if they are not the same
                        {
                            resolvents = resolve(clauses[i], clauses[j]);
                            if (resolvents.Count == 0) //empty
                                return true; //solved
                            newItem = union_clause_sets(resolvents, newItem);
                            //if (!containsClause(newItem, resolvents)) //if not already in newItem
                                //newItem.Add(resolvents); //Union
                           //newItem = newItem.clauseUnion(resolvents); //suspect?
                        }
                    }//end inner for loop
                }
                    //if newItem is a subset of clauses
                    //if every item in newItem is contained in clause
                if (is_a_subset(newItem, clauses)) // is newItem a subset of clauses
                    return false;

                clauses = union_clause_sets(clauses, newItem);
            }
        }

        private bool containsClause(List<Clause> haystack, Clause needle)
        {
            foreach (Clause c in haystack)
            {
                if (c.is_same(needle))
                    return true;
            }
            return false;
            //throw new NotImplementedException();
        }

        private List<Clause> union_clause_sets(List<Clause> clauses, List<Clause> newItem)
        {
            List<Clause> return_clause = new List<Clause>();

            return_clause = clauses;

            foreach (Clause c in newItem)
            {
                if (!containsClause(return_clause, c))
                    return_clause.Add(c);
            }//end foreach
            //throw new NotImplementedException();
            return return_clause;
        }

        private bool is_a_subset(List<Clause> possibleSubset, List<Clause> set)
        {
            //every item in newItem is contained in clauses
            foreach (Clause c in possibleSubset)
            {
                if (!containsClause(set,c))//is not contained in clauses
                    return false;
            }
            return true;
        }

        /// <summary>
        /// resolve - this returns a clause
        /// </summary>
        /// <param name="c1">first clause</param>
        /// <param name="c2">second clause</param>
        /// <returns>a clause</returns>
        private List<Clause> resolve(Clause c1, Clause c2)
        {
            List<Clause> resolvents = new List<Clause>();//new Clause(main_model);
            //resolvents.Add(c1.clone());
            Clause tempClause = new Clause(main_model);
            Clause baseClause = c1.clone();
            tempClause = new Clause(main_model);

            if (c1 == c2) //if they are the same
            {
                resolvents.Add(c1);
                return resolvents;//return one of them
            }

            //merge c1 and c2 to form resolvents list
            foreach (Literal l in c2)
            {
                if (!c1.contained_in(l))
                    baseClause.Add(l);
            }
            tempClause = baseClause.clone();
            bool seenNegation = false ;
            foreach (Literal lit1 in c1)
            {
                foreach (Literal lit2 in c2)
                {
                    if ((lit1.SymbolName == lit2.SymbolName) && (lit1.isNegation != lit2.isNegation))
                    {
                        seenNegation = true;
                        //remove lit1 and lit 2
                        //if(resolvents.Contains(lit1))
                            tempClause.remove(lit1);
                        //if(resolvents.Contains(lit2))
                            tempClause.remove(lit2);
                            if (tempClause.Count != 0) //if clause is not empty
                            {
                                if (resolvents.Count == 0) //is empty
                                    resolvents.Add(tempClause);
                                else if (!containsClause(resolvents, tempClause)) //if it is not already in the set
                                    resolvents.Add(tempClause);
                            }
                            tempClause = new Clause(main_model);
                            tempClause = baseClause.clone();
                    }
                }
            }
            if (!seenNegation) //nothing was eleminated
                resolvents.Add(baseClause);
            return resolvents;
        }

        /// <summary>
        /// run resolution button
        /// </summary>
        /// <param name="sender"></param>
        /// <param name="e"></param>
        private void runResoluion_Click(object sender, EventArgs e)
        {
            if (resolution(set_of_clauses))
                MessageBox.Show("Resolved [Using Resolution Algorithm]");
            else
                MessageBox.Show("Resolution Failed");
        }

        private void toolStripButton1_Click(object sender, EventArgs e)
        {
            MessageBox.Show("Type in: \n - (hyphen) for negation and | for OR\n ex:\n-a | b\nb | -c | d\nThen click add clause.\nNumberical values are not acceptable.");
        }//end resolve function
    }
}
